Repository navigation
WHIR no-epoch (prove-and-retire) prover: block 25368371 — work in progress - #1014
Draft
MauroToscano wants to merge 1901 commits into
Draft
MauroToscano wants to merge 1901 commits into
MauroToscano wants to merge 1901 commits into
Conversation
|
Benchmark Results for modified programs 🚀
|
|
Benchmark Results for unmodified programs 🚀
|
MauroToscano
force-pushed
the
noepoch/whir
branch
from
October 1, 2026 14:57
e9107c6 to
97ba486
Compare
MauroToscano
added a commit
that referenced
this pull request
Oct 2, 2026
… leaves The builder kept every walked window until finish, so at the run's end all of its op lists were resident, about 300 B per cycle (0.28 GiB per M cycles: 8.6 GiB on block 25368371 and about 100 GiB on a median mainnet block). WindowedTraceBuilder::drop_streamed_ops keeps only the ops not yet in a handed-out chunk for each of the 8 streamed tables (Tail: the windows' lists moved in whole and freed once used up). As a chunk leaves, the builder takes what the table phase would have read from its ops. It counts BITWISE's lookups from LT, SHIFT, STORE, MEMW_A and MEMW_R, plus DECODE's lookups and the last ECALL from CPU. It derives and keeps the phase-3 LT ops of MEMW and MEMW_A, unless stream_memw_lt already put them in the windows' LT lists. The other walk lists are appended window by window instead of being concatenated at finish. The in-walk BITWISE lookups are counted and dropped. finish runs the table phase over the tails (StreamSkip::tails), padding the dropped CPU chunks and placing the kept LT ops where phase 3 would have derived them. The tables are the same. The new tests compare every table with the whole-run build, and with stream_memw_lt every table with the builder that keeps its windows, plus LT's multiplicities. Both go through push and the split, at window lengths 1 to the whole run, and with chunks small enough that all 8 tables drop. The same comparison runs with KECCAK_RND streamed. Another test checks that after each window each table holds less than a chunk of ops. Removing any one accounting step (LT, MEMW_R or DECODE counts, the CPU padding, either LT prefix) fails the first test. Off by default. Cherry-picked from mem/m1 74e1df1 onto #1014, with the streamed finish's build marks kept.
MauroToscano
added a commit
that referenced
this pull request
Oct 3, 2026
MauroToscano
added a commit
that referenced
this pull request
Oct 3, 2026
…es are laid out #1014 now lays the streamed chunks out on three workers (0498480), and phase A waits on the groups the rest closes, which close only once the whole rest is laid out. With b1's waves the AIR order's prefix is laid out first, so pack_rest_as_laid_out (the rest's sink, groups identical by test) is now on in production: each wave's tables go to the packer as the wave ends, and a group closes once its own tables are laid out. Laid out all at once, the first table in AIR order was ready only with the last, which is why packing as laid out read +0.21 s before (FAST 422). The real-block tests' BLOCK_WHIR_PACK_REST=0|1 now overrides the production choice instead of replacing it with off. Readouts for the finish's place in phase A: each group's commit start (from@, beside done@), and every rest table's layout end and group in AIR order (BLOCK REST TABLES).
MauroToscano
added a commit
that referenced
this pull request
Oct 3, 2026
MauroToscano
added a commit
that referenced
this pull request
Oct 3, 2026
MauroToscano
added a commit
that referenced
this pull request
Oct 3, 2026
MauroToscano
added a commit
that referenced
this pull request
Oct 3, 2026
MauroToscano
added a commit
that referenced
this pull request
Oct 3, 2026
…s its tables, the block memory log) into nw2/r2ii No conflicts. multilinear_block.rs: the memory log's phase-B marks and the group observer sit side by side at the end of each group (the observer first, then the group's columns are released and the mark taken). block_whir.rs and the W3 harness: the new BlockOptions fields and the memory log's plumbing next to the group observer's.
MauroToscano
added a commit
that referenced
this pull request
Oct 3, 2026
… proof to an observer; the block tree's first leaf executes during phase B) into m4b/b2 No conflict. R2-ii's two full BlockOptions literals in lfm/whir_block_tests.rs already carry b2's pack_finished: true, so its hand-over tests run with the finish's tables packed, as production does.
MauroToscano
added a commit
that referenced
this pull request
Oct 3, 2026
…14fea1 crypto/stark/src/narrow.rs and crypto/stark/src/spill.rs are #1013's files, byte-identical to mem/stark-f1 @ e5214fea1 (i-mem3's F1: the page-backed Bytes, the streaming Digester, the fused writer, over the S1/S2 store). #1013 is their one source of truth: #1014 never edits them, re-imports any change from there, and they merge as one when both PRs reach main. Wiring only: the two modules in lib.rs (dead code allowed there, since some parts serve #1013's prover alone), math's page-bytes feature, and libc unconditional as the store needs it (it was behind disk-spill). #1013's prover glue (TraceTable::spill_main) and its spill tests are not imported; #1014's adapter and tests follow.
MauroToscano
added a commit
that referenced
this pull request
Oct 3, 2026
… reserve LAMBDA_VM_BLOCK_SPILL now reads as #1013's (prover/src/block.rs SpillPolicy … spill_decision @ edddc68): auto (and unset) | off | always | <GiB> resident budget. auto spills a committed table once the host's bytes (the larger of VmHWM and the cgroup's memory.current), the reserve and the table would pass the target (LAMBDA_VM_BLOCK_SPILL_TARGET_GIB, else the cgroup's memory.max less 10 GiB, else MemTotal less 10 GiB). Phase A decides per table and never past the writers' queue; groups 0 and 1 count but never spill. The reserve is #1014's own, inferred from the median block (BIG 565): the finish's p5 transient (25.5 GiB) and the tree's leaf programs alive through phase B (16.3 GiB), about 1.25 GiB per total G cells or 1.65 per G cells committed so far, plus 6 GiB for phase B's bump and the read-back window. BlockSpill carries the policy's choice (SpillWanted) and the kept bytes and committed cells it reads. A block that fits spills nothing; the store opens for every policy but off. Tests: the knob and the decision (unit), a budget the block fits in spills nothing and one of zero spills (block).
MauroToscano
added a commit
that referenced
this pull request
Oct 3, 2026
…@ 278e6a8 The rule #1014 copies from #1013 read only cgroup v2's memory.max and memory.current. On a v1 host (FAST) the target fell through to MemTotal less 10 GiB, and the host's charge was not read at all. #1013 fixed both in 278e6a8; this re-copies spill_target_bytes, spill_target_from, cgroup_memory and host_bytes_now from that sha, with its two tests (the cgroup files from fake trees, and the target rule), cited as before. The only changes from #1013's text are the citations and the tests' temporary directory, which gets a name of its own so the two copies of the test never share one if they ever run in one process.
MauroToscano
added a commit
that referenced
this pull request
Oct 3, 2026
…cf253d2) The host measure #1014 copies from #1013 took max(VmHWM, the cgroup's charge), and the charge counts page cache. FAST charged 40.58 GB at 17:28Z with 15.18 GB of it inactive file pages, which would have made auto spill the last groups of a 1x block that fits. This re-copies #1013's measure from its landed head 035aef5 (commit cf253d2): HostReading reads VmHWM, the charge and memory.stat's inactive file pages (v2 inactive_file, v1 total_inactive_file, by their exact key), and the host's bytes are max(VmHWM, charge - inactive_file). CgroupValue lets cgroup_memory read a whole-file number or one memory.stat key. The BLOCK SPILL line ends with the largest reading auto decided on, as #1013's does. With #1013's two tests; the text differs only in citations and the test's temporary directory. The rest of #1013's train (lazy queue budgets, the allocator purge) is not copied: #1014 has no queue budgets.
MauroToscano
added a commit
that referenced
this pull request
Oct 4, 2026
MauroToscano
added a commit
that referenced
this pull request
Oct 4, 2026
MauroToscano
added a commit
that referenced
this pull request
Oct 4, 2026
The spill code (stark, multilinear, block_whir) and the streamed top (executor, proof, the W3 tree) touch disjoint code; the one shared file, whir_block_tests.rs, merges without conflict (the spill side adds BlockSpillPolicy::Off to two test fixtures).
MauroToscano
added a commit
that referenced
this pull request
Oct 5, 2026
MauroToscano
added a commit
that referenced
this pull request
Oct 5, 2026
MauroToscano
added a commit
that referenced
this pull request
Oct 5, 2026
…114; min proven bits unchanged at 130.393) The default flip of LAMBDA_VM_ZF_WHIR_GRIND_BITS: the port of #1010's 5364aa2 and its pin follow-up 2687e48. PRODUCTION_WHIR_GRIND_BITS is 18; LEGACY_WHIR_GRIND_BITS = 20 keeps the legacy format and is the opt-out (LAMBDA_VM_ZF_WHIR_GRIND_BITS=20). It reaches #1014's WHIR proofs: the block's group chains and prepared openings, verify_block_whir, and the W3 leaves' in-guest verifier. The W3 tree's own STARK LFM proofs do not read it. The binding WHIR phase is unchanged (the unground fold at 27 variables, 130.393 bits); the query phases move 130.926 -> 130.907. Measured behind the knob on c55dec4: ULTRA 019 1x phase B -0.344 s (t -12.9), whole -0.270 s, recursion -0.010 s; BIG 628 median whole -3.42 s, both arms verified. The opt-out reproduces the previous 1x proof byte for byte (top digest 0da6fea9 under fixed hash keys and deterministic grind); the new default's is b9b4826d. The W-leg sizing pins follow the process's grind bits, as 2687e48 did on #1010.
MauroToscano
added a commit
that referenced
this pull request
Oct 6, 2026
…all, commit pairs off the pool) ULTRA 096 (median 25475471, #1014 + cap 256, one binary, 3 + 3 runs plus 2 + 2 single-lever arms) read LEVER EFFECTIVE on every pre-registered row: phase-A end -6.66 s with every run of the pair below every run without it, whole block -6.86 s (154.67 -> 147.81 s), finish 15.8 -> 9.3 s at most, KECCAK_RND's span 12.0 -> 5.4 s at most, the largest phase-A commit 2.93 -> 0.68 s, the card's wait for the rest 6.65 -> 1.77 s, max RSS -0.97 GiB. The wave alone gave -5.92 s whole, the commit pairs alone -0.47 s. At 1x (ULTRA 095) the pair is neutral (whole -0.016 s, t -0.4) and the top digest is unchanged. Both become the defaults; the knobs stay as opt-outs: LAMBDA_VM_KR_PACKED_WAVE=4 builds the chunks four at a time again, and LAMBDA_VM_BLOCK_COMMIT_OFF_POOL=0 puts the commit pairs back on the global pool. The proof bytes are the same either way.
MauroToscano
added a commit
that referenced
this pull request
Oct 6, 2026
…W_WINDOW=1) A #1014 block leaf's LFM_BALU is 70,692 rows a full group, so a 4-group leaf holds 282,768 rows and pads to 2^19. 34,200 of a group's rows are the lean fold's point x0^-1 = prod g^(-2^i b_i): one Select and one Mul a bit through edsl::pow_bits. pow_bits_windowed drops the identity multiply (the first factor read is the accumulator) and reads each of the first two bit pairs through a 4-way Select mux over the constants {1, f0, f1, f0 f1}. A fold then pays three fewer Muls and two more Selects at four or more index bits, two and one below. A full group goes -6,498 LFM_BALU and +4,104 LFM_SELECT, so a 4-group leaf's LFM_BALU drops to 256,776 (under 2^18) while its LFM_SELECT stays under 2^19 at 480,168. The value is the same and so is the Select semantics. The knob is read at program emission like LAMBDA_VM_WHIR_FOLD_CLASSIC and defaults off, so today's programs and ids are unchanged. pow_bits itself is untouched, so the STARK paths keep their programs. The lean fold's row and constant closed forms follow the setting.
MauroToscano
added a commit
that referenced
this pull request
Oct 10, 2026
…E_DOWNLOAD (default off) The port to #1014 of #1013's 6d25865: the same changed lines in device.rs, lde.rs, stark's gpu_lde.rs and the new device test, applied to functions that were identical on both PRs. On a precomputed-tree cache miss the preprocessed commit downloads the full node buffer into a zeroed pageable Vec<u8> and stark copies it once more into Vec<[u8; 32]>. #1014's median recursion pulls about 14.7 GB this way at 2.75 GB/s (I-PROF4 B.5.1). LAMBDA_VM_TREE_DOWNLOAD=staged sends it through a staging pair straight into the node vector and queues the multiplicity tree behind the last chunk; the device peak stays one tree and the nodes are the same bytes.
MauroToscano
added a commit
that referenced
this pull request
Oct 10, 2026
The port to #1014 of #1013's 814a4b6. LAMBDA_VM_TREE_DOWNLOAD unset (or any unknown value) now selects the staged download; `legacy` or `pageable` keeps the old pageable copy as an opt-out. The nodes are the same bytes on both paths. A unit test pins the default. On #1013, legacy vs staged on the median 25475471, one binary per job: recursion -2.94 s (t -15.9, ULTRA 094) and -6.26 s (t -27.6, RYZEN 002), with the base digest and the top program id unchanged (ULTRA 093, 100). #1014's own gate is I-COPIES §10.
…fusals The chunking rule's invariants over every count to 2,100 (the chunks cover the interactions, fill today's slots with the all-padding chunks, and a cut always saves at its price), its cuts on the base's table shapes, the combined claim against the padded layer's extension, and round trips of tables cut every way the rule allows. Under the packing: a short or extra tree, a proof laid out at another price, a chunk's output or halves off by one, chunks swapped, a forged balance and a tampered combined claim are refused; neither format's verifier takes the other's proof, and with nothing cut the packed proof is today's, byte for byte. The card proves the host's bytes on cut tables, and at Off the prover lays out one tree a table over its own list. On the block: the knob reads off or a price, the verifier's packing is a named constant, and a packed block proves, verifies and refuses today's format both ways.
A stark build with `cuda` but not `multilinear/cuda` has a card the batched argue's device paths cannot reach: every tree and round falls to the host, and each card-against-host byte check passes on the host against itself. The three card tests (today's batched argue, its round slot, and the packed argue) now probe the card with math-cuda directly and refuse to pass when one is present and the argue's device paths are not built.
… cells
The production batched argue now lays its LogUp-GKR trees out under
GkrPack::PRODUCTION (Chunks { tree_log_cells: 22 }): a table whose
power-of-two padding costs more input cells than the trees a cut would
add, each priced at 2^22 cells, is argued as equal chunk trees. On a
block that cuts CPU, MEMW_A and SHIFT in three and KECCAK_RND in five.
ArgueFormat::BATCHED and ArgueFormat::batched(cap) carry it, so the
prover's and the pinned verifier's block formats, the recursion's
in-guest verifier and the tree presets all take it from the one
constant. GkrPack::Off, one tree a table, stays selectable everywhere.
- CLI: prove-block and verify-block default to --argue-pack 22; `off`
is the unpacked format.
- Harness: BLOCK_WHIR_ARGUE_PACK unset keeps the format's own packing,
`off` or a price replaces it.
- The tree harness verifies a run at the production packing with the
public grouped verifier, and any other packing through its named
presets.
Pins: the median-mix leaf programs are re-pinned at the production
packing (both query checks); their Off rows keep the previous digests,
so the unpacked programs are unchanged. The batched argue's byte pins
and the phase-B proof pins do not move: no table in those fixtures is
cut at this price, and an uncut packed proof is the unpacked one, byte
for byte. Tests that mean the unpacked layout now name GkrPack::Off.
With the knob at 1 a streamed prove records, for the run's first 48 windows, when the pass took each from the executor, passed it and handed it out, when a walker walked it (and how much of that went on seeding its entries) and when it was absorbed; for the first 128 streamed chunks, when each was handed out, laid out and placed; every chunk's layout seconds by table; and when the card's early setup ended. Four BLOCK HEAD lines print as phase A ends and ride BlockStamps::head. The prove also names how the card is set up in a BLOCK CARD EARLY banner (LAMBDA_VM_BLOCK_CARD_EARLY, unchanged). Nothing is recorded with the knob off, and no proof byte moves either way.
LAMBDA_VM_BLOCK_CARD_EARLY was opt-in. The card's context, modules and staging pools now come up on a thread of their own as the streamed prove starts, in a build with the card's kernels, unless the variable is 0, off or empty, which sets the card up at its first use as before. The proof's bytes are the same either way. Alone it moves no time, since the setup already overlapped the wait for the second group; it pays once the first groups close sooner.
LAMBDA_VM_BLOCK_CARD_FILL's default in a build with the card's kernels now holds every full streamed chunk of MEMW_A, LOAD, STORE, MEMW and SHIFT as its rows and lets the card fill its columns, as CPU and MEMW_R already were, taking their wide layout off the host's layout workers. The words, and so the proof's bytes, are the same. The earlier default stays one word away, keccak_rnd,cpu,memw_r; a build without the card is unchanged. The tests that ask for CPU and MEMW_R records alone now say no row family too, so they read the same with either default.
A new chain format value, `ChainFormat::round0`: `Each` (the default, today's bytes) commits one round-0 tree a stacked polynomial; `One` commits a grouped run of P' >= 2 polynomials as ONE tree whose leaf at block j hashes the run's P' blocks j end to end, under the Poseidon1 leaf tag with the block count in its third lane ([len, LEAF_DOMAIN, P', 0]). A query then opens one leaf and one path instead of P' of each; at a run of three and a first fold of six that is 16 permutations a leaf position instead of 18, and one inner tree instead of three. The choice is a verifier constant: bit 45 of the fold word binds it into the statement, `round0_trees` derives which polynomials share a tree from the layout and the config, and the verifier refuses a joint opening (`RoundOpenings::BaseJoint`, appended) wherever a per-tree one is expected and the reverse, a root count other than its own, and a leaf of another width before any path is read. It needs grouped chains and Poseidon1 trees, refused otherwise. The card commits a joint run in one leaf launch over its encoded codewords (`p1s_leaves_base_coset_joint` and its lean twin) and keeps the tree's nodes until the retire; a revived joint tree re-hashes its queried blocks from the run's stacks or, with the stack path off, from the re-encoded codewords. The round-0 leaf permutations the card's commits pay are counted (`gpu::commit_leaf_perms`).
…_WHIR_TREES A new process-format knob, `LAMBDA_VM_ZF_WHIR_TREES=each|one` (`ZfFormat::whir_trees`; unset is `each`, today's bytes), stamped onto the block's chain config alone by `BlockFormat::chain_config`. Under `one` each block group's run of stacked polynomials commits one round-0 tree (the chain format's `Round0Trees::One`); it is refused under another base than Poseidon1 or the natural leaf order, and the banner names it off the default (` whir_trees=one`). The pinned verifier keeps one tree a polynomial. The block's roots are now one a round-0 tree, its commit-time answers still one a polynomial: the block verifier and the multi-proof verifier slice the roots by `round0_trees` and the answers by polynomial, and a group's commit-time point is drawn over its trees' roots. The recursion follows the same format from its config: the chain shape knows a joint round 0 (one tree, one leaf of P' blocks a query, one cap), the leaf hashes it under the joint tag (`joint_leaf_hash` and its word form), walks one path and combines the leaf's blocks; the arena lays a joint opening out as a polynomial's own; the block leaf carries one root a tree and one answer a polynomial; the plan prices a group's commit-time point over its trees. The real-block harness prints `W3 WHIR TREES` (the mode, the round-0 tree count against the polynomials, and the round-0 leaf permutations the card's commits paid).
…t alone The joint-tree card test read the round-0 leaf permutations across the commit and the opening; an opening that rebuilt an evicted tree would have counted its leaves again. The count is now taken around the commit, which is what it pins.
A caller may move the leaf order after the knobs were read (`prove-block --leaves natural` beside LAMBDA_VM_ZF_WHIR_TREES=one), and `install` checked only the implemented levers and the LFM merge. It now runs `check_trees` on the format it is about to install, before anything is installed. The refusal's message is one line again.
…t order multilinear: each step of the argument for one round-0 tree a run as a test of its own: the joint leaf is the spelled-out rate-12 chain with the block count in its first input; the fold word is injective over the chain's formats; inside a stack the joint verifier's transcript calls are the per-tree verifier's, call for call; at the verifier's positions block p of a joint leaf is polynomial p's coset block; swapped blocks, a joint opening at a lone polynomial and a mode the config lacks are refused. prover: the in-guest joint leg under the coset order, the block's production order, at runs of two, three and four and a [4, 2] split, uncapped and capped: the accepted proof executes, and a value in slot 1, swapped blocks and a path node have no execution under either the per-query or the lean check. The cross-leg test's doc now says arena length is a shape fact, not the soundness mechanism.
KECCAK_RND argues 1,031 interactions, so its LogUp-GKR input pads to 2,048 slots, or to 5 trees of 256 under the packed argue. Its 20 ARE_BYTES checks on Cxz_left are implied by lookups it already sends: - each Cxz_left byte enters a BYTE_ALU[XOR] D lookup (operands are bytes), as itself for odd bytes and plus a carry bit for even ones; - that leaves an even byte one extra value, -1; - the theta identity 2*in = 2^16*carry + 256*hi + lo then rules -1 out by parity, since every term is below 2^18 and so it holds over the integers; - on padding rows (mu = 0) nothing reads Cxz_left. Dropping them leaves 1,011 interactions: one tree of 1,024 slots. A new format value, BlockFormat::keccak_rnd (KeccakRndForm::Full by default, Lean opt-in), selects the table's interactions in the block's AIR set. block_frame follows it, so the verifier and the recursion's leaves follow it too, as does the prover's streamed AIRs. The windowed builder's BITWISE count follows it, its padding rows' byte checks included (200 a row instead of 220), and so does the KECCAK_RND split's take-back. The whole-run build counts today's table only and refuses Lean. The whole-block harness reads BLOCK_WHIR_KECCAK_RND=lean (unset or full is today's) and prints the form. The verifier presets hold Full. Columns, constraints, the card fill and every proof at the default are unchanged. Tests: - the lean list is today's less exactly the 20 checks; - every Cxz_left byte still enters a mu-weighted D XOR lookup; - an exhaustive check that a low byte of -1 breaks the identity for every halfword, carry and high byte, and its mutation without the factor 2 admits one; - the presets hold Full; - a lean block proves and verifies while each form's verifier refuses the other's proof.
The AIR prototype cache is keyed by table name and proof options, on the premise that under one name a table's interactions are fixed. The lean form broke that premise: both forms were cached as KECCAK_RND, so the first one built in a process was served to every later caller. In a block gate the lean prover's AIR reached the full verifier, which then accepted the lean proof. A verifier in a fresh process builds its own form and was not affected. The lean prototype is now cached as KECCAK_RND~lean, and its clone is still named KECCAK_RND. A test builds the two forms in turn in one process and checks each keeps its own interaction count. The lean block test's cross-check now refuses as it should: the full verifier reports a ladder shape mismatch on the lean proof.
Adding the lean KECCAK_RND tests' module beside them dropped the cfg(test) and cfg(feature = "parallel") lines above block_whir_pack_tests. Put them back.
prove-block read BLOCK_WHIR_KECCAK_RND through the tree config without a check, so the environment could switch the CLI prover to the lean form, and verify-block, which holds its preset form, would refuse the proof only after the whole proving run. The CLI now refuses the knob by name, as it refuses BLOCK_WHIR_ARGUE_PACK. at_presets also requires the format's form to be the pinned preset's, and its test gains a row for the other form. The another-tree message names the knob too.
The environment pin now sets BLOCK_WHIR_KECCAK_RND=lean as well. Under it, the child asserts that the harness's format follows the knob, and that the pinned verifier presets and the named-choice presets keep their Full form.
The module doc, the interactions' section header and the constraint set's doc still said that the θ shift outputs' ARE_BYTES checks bound the decomposition, and counted 1,031 interactions. Under the lean form those checks are gone. There the range comes from the D lookups' byte operands and the identity's parity, while the ρ checks stay load-bearing in both forms. The D lookups now carry a note that, under the lean form, they hold the Cxz_left range.
…ation The lean tests checked the θ parity argument on a model of the identity only, so nothing failed if the AIR's θ entry changed. Three tests now run the real constraint set on real trace rows against the real interaction lists: - every other (lo, hi, carry) that keeps all 141 constraints on a real row sends a D lookup with a non-byte operand under the lean form, and an ARE_BYTES pair off a byte under the full form; - the mutation: with the D lookups that read Cxz_left removed, a forged decomposition keeps every constraint and sends nothing off BITWISE; - the AIR's θ entry is exactly the identity the model checks, for any field values, and is zero when mu is zero.
…uilt with The AIR prototype cache is keyed by table name and proof options and rests on a name fixing its table's interactions. Keeping two KECCAK_RND forms apart depended on giving the lean one its own name, so a later table whose interactions vary under one name would be served the wrong list. On a hit, the cache now compares the cached prototype's interactions with the ones handed in. It serves the clone only when they are equal. Otherwise it builds the handed list uncached and leaves the entry alone, so nothing panics on a verifier path. BusInteraction, BusValue, Multiplicity and LinearTerm derive equality for the comparison; no format changes. A test builds two lists under one name in turn and gets each back.
BlockFormat::production() and pinned() now hold KeccakRndForm::Lean, so the block prover and every preset verifier use KECCAK_RND without the 20 byte checks its D lookups imply (1,011 interactions, one 1,024-slot GKR tree under the packed argue). Full stays the type's Default. That is the form of every build outside the block format (the whole-run builder, which refuses Lean, the LFM machine's own chips, the in-guest continuation verifier) and the variant a block caller may still name. The harness's BLOCK_WHIR_KECCAK_RND, when unset, now follows the pinned preset, so the harness proves what verify-block verifies. The CLI still refuses the knob, and at_presets already compares against pinned(). The environment pin sets the knob to full and expects the harness Full and both verifier presets Lean. The soundness comments describe Lean as the presets' form and Full as the variant. The median-mix leaf-program pins move with KECCAK_RND's interactions and are re-blessed (first and last leaf, both query checks, packed and unpacked).
A verifier that derives a commitment of its own, the block's prepared stacks (DECODE and the dense genesis pages), committed it with the same path a prover takes: on the card in a card build, at a stack of 2^16 or more. So a card kernel's output decided what the verifier accepted. The host block verifier (`commit_groups_on_host`) and the recursion's verifier plan (`commit_prepared`) now commit those stacks on the host (`StackedCommitment::commit_on_host`, with `commit_stacked_on_host` and `commit_joint_stacked_on_host`). The roots are the same: the card's kernels are checked against these host functions. The prover keeps its card commit and hands its own roots to its plan, so proving time does not move. Tests: the host commit has the commit's roots under either round-0 format and leaf order; on a card, it has the card's roots and runs no card commit and no card leaf pass. An ignored instrument prints what the host derivation costs over stacks shaped as the prepared tables.
How many round-0 trees a group's chain commits becomes a choice the block commands and the public verifier name, as the leaf order is: - `prove-block --trees each|one` and `verify-block --trees each|one`, installed with the process format. Unset, the format's default, except under `--leaves natural`, where it reads `each`: one tree a run is defined for the coset order alone. `LAMBDA_VM_ZF_WHIR_TREES` in the environment is refused by both commands; - `verify_whir_block_tree_proof_at` and `verify_block_tree_at` take the trees; `verifier_presets_at` sets them and runs `check_trees` beside `check_leaves`, so one tree a run under the natural order has no presets, whichever leaf order the caller named; - the process format's knob, unset beside the natural order's word, reads `each`, so the order's rollback keeps parsing on its own. The proof carries none of it. Tests: both commands parse the two words, refuse any other and refuse one tree under the natural order at install; the presets at the other trees derive another block id over the same statement, a prover of those trees claims it, and one tree under the natural order has no presets.
A run of three stacked polynomials of 2^27 at blowup 2 in the coset order commits one joint tree of 2^22 leaves. The card's root must equal the host commit the verifiers use, the leaves must cost exactly 16 permutations each, and nothing may fall back to the host. The existing card cases stop at 2^14 leaves, so this covers the shape every production group commits once one tree a run is the default.
ZfFormat::DEFAULT now commits each grouped run of a block group's stack as one round-0 tree (Round0Trees::One). A leaf holds the run's coset blocks end to end, so a run of three pays 16 leaf permutations a position instead of 18 and a query opens one path instead of three. Production, the pinned verifier presets and an unset --trees on prove-block and verify-block all take it. LEGACY keeps one tree a polynomial. The off spelling is LAMBDA_VM_ZF_WHIR_TREES=each (or --trees each), and the banner now prints whir_trees=each off the default. Under the natural leaf order, where one tree a run is not defined, the knob unset reads each and the banner names no trees; one named beside it is still refused. BlockFormat::chain_config stamps the trees only under one chain a run. One chain a polynomial has no runs, so its trees stay one a polynomial whatever the knob says; with the new default a per-polynomial format would otherwise fail with JointTreeUnsupported. Tests: the ones whose subject is one tree a polynomial now name it. These are the root-for-root comparison of one chain a run against one chain a polynomial, the natural-order arms, and the grouped-forgery and grouped prepared-chain leaf tests. One tree a run's round trips, leaf executions and forgeries now run at the default. The run-width helpers read joint openings, and the CLI banner test covers --trees. Pins: the median-mix leaf programs move (a joint leaf, one path a query, the fold word's one-tree bit) and are re-blessed. Under the lean query check the median mix needs four leaves instead of five, and the one-top scale's first level is [3, 1] instead of [3, 2].
…ack after a tree The card permit's arming is process-wide. Its own unit tests serialised only among themselves, through a module-local lock, while the block tree arms it with its sibling count and the tree tests reset it to one. In one test process, a tree test beside a permit test could re-arm the permit under it, and a tree left the permit armed for whatever ran next. - `PERMIT_TEST_LOCK` is the crate's one lock for the permit. The permit tests take it, and so does every tree test, through `serial_for_test` (taken through a poisoned lock, permit back to inert). - The tree arms the permit through `arm_scoped`, which puts back what it found when the tree returns. No proof byte moves; production arming is unchanged while the tree proves.
…'s failure On a loaded test process the permit tests failed four at a time. Three of them assert that a prove "did not wait" by holding it to 100 ms of wall clock, which a busy machine exceeds without any wait. Each test also took its lock with `expect`, so the first failure poisoned the lock and failed every permit test after it. - "Did not wait" now means under half the deferral bound. A prove that waited for a shut latch is held to the whole 30 s bound; one that did not is never near it. - The opener test's open latch is held to half its own bound the same way. - Each test takes the lock through a poisoned one. The lower bounds (a waiter waited at least its pause) are unchanged.
…ount their fills `multilinear::records::fills()` is a process-wide count, and each prove stamps its difference across its own window. Three tests assert that difference exactly: (0, 0) with the knob off, and each held table filled on the host once. In one test process, a records table that another test fills inside that window moves the count, and the test fails although its own prove is right. The twelve block tests that hold tables as records (KECCAK_RND, the streamed CPU and MEMW_R chunks, the row families) now take one lock. That includes the three that count, so no other records fill can land inside a counting window. The lock is taken through a poisoned one.
…run test_ecrec `FORGE_ECREC_SWAPPED_CHAINS` is a process-wide switch, keyed on `test_ecrec`'s first `r`. Its doc said tests beside the forging one are unaffected, but that holds only for tests running other programs. Any test that runs `test_ecrec` while the switch is set builds the forged call. Its neighbour `ecrec_chains_are_keyed_apart_on_the_bus` proves the same guest, and libtest starts the two side by side. - `ECREC_FORGE_TEST_LOCK` is a read-write lock. The forging test holds it to write while it sets the switch. - Every other test that runs `test_ecrec` holds it to read through `ecrec_forge_free`, so they still run beside one another. That is twelve tests: the keyed-apart block test, and the trace builder's and the bus checks' program-list tests. - The switch's doc now says what it reaches and how the tests stay apart.
`a_table_handed_on_last_does_not_hold_back_the_rest` and `a_slow_table_holds_back_only_the_hand_on` read the hand-on against the wall clock (a table handed on before 400 ms, the slow one after 600 ms). They built their tables on rayon's global pool. In one test process that pool runs other tests' proves, and a table's build waits behind them, so the first hand-on missed 400 ms with nothing wrong in the stream. Each test now installs a six-thread pool of its own and runs on it. The bounds and the assertions are unchanged.
…sites `note_device_fallback_is_called_at_exactly_the_five_argue_sites` still expected one call in columns.rs. The group upload's records fill brought three more in `DeviceColumns::upload_tables`, so the test failed at every head since: - its room; - its staging promise for a packed or records table; - its fill checks (a records table whose log the card refused: the card declines the group and its readers take the host's columns). Each moves the work to the host, which is what the counter is for, so the census now counts all four: (3, 1, 4). The counter's doc lists the nine sites, the eight in math-cuda by function, and widens its scope from reservation refusals to the declined fill as well. The test is renamed to the eight sites it checks.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
One WHIR (multilinear) proof per block, with no epochs (the prove-and-retire / VADCOP shape). This is a second prover next to #1010's epoch-based one. #1010 stays the reference and this branch does not touch it. The branch starts from #1010's head
f3d359998; compare againstf3d359998to see only this work.What it is
prover::block_whir::prove_block_whir/verify_block_whir. The whole block is oneMultiProof:(z, α, β)are drawn once.S_post ‖ g: upload again, argue (LogUp-GKR), re-encode with the NTT alone, open. The dropped tree levels are rebuilt from the queried cosets and checked against the kept nodes.WindowedTraceBuilder(noepoch/windowed-builder, also used by STARK no-epoch (prove-and-retire) prover: block 25368371 — work in progress #1013). Every full chunk of CPU, MEMW_R, MEMW_A, MEMW, LOAD, LT, SHIFT and STORE is laid out and committed as soon as it exists.⚠ Format changes (all approved by Mauro, 10-02 (§7 on 10-05), but §6, the port of #1013's S0a; for the cryptography team's end review; ledger rows W-0…W-6, W-8, W-9 in CRYPTO-REVIEW.md)
The block is one WHIR proof (
BlockWhirProof, oneMultiProof) over all of the block's tables.z, α, β.S_post ‖ g).Every parameter below is a verifier-side constant. None is read from the proof.
BLOCK_GROUP_POLYSBLOCK_MAX_GROUPSBLOCK_MAX_TABLE_VARSBLOCK_MAX_KECCAK_RNDBLOCK_KECCAK_RND_MAX_VARSBLOCK_MAX_ECDASBLOCK_ECDAS_MAX_VARSBLOCK_MAX_KECCAKBLOCK_KECCAK_MAX_VARSBLOCK_MAX_ECSMBLOCK_ECSM_MAX_VARSArgueFormat::BATCHEDPRODUCTION_WHIR_GRIND_BITSLEAF_PERMS_CAP,BLOCK_FAN_IN1. The group partition is in the statement
What. The streamed prover packs tables into groups in the order their chunks complete. It writes the partition (per group, its tables' indices) into the statement. The transcript absorbs it before any root.
Verifier. The verifier checks:
It then rebuilds every group's stack layout itself.
Security. Proven bits are unchanged.
BLOCK_MAX_TABLE_VARS(change 3), so no partition can make a chain taller than 2^27.Proof bytes vary from run to run. Arrival order depends on thread timing, and the hash-ordered tables' row order (LT, EQ, BYTEWISE, BRANCH, MUL, DVRM) follows a hash state that is random per process. Mauro, 10-02: "the proof not having the same bytes it's fine, they never had the same bytes anyways".
LAMBDA_VM_FIXED_TRACE_HASH=1(fixed hash keys) andLAMBDA_VM_DETERMINISTIC_GRIND=1. Under both, two processes prove the same bytes (FAST 423).2. Prepared openings, one stack per group (approved by Mauro, 10-02: "it's a standard technique, go ahead")
In short. This is #1010's existing prepared DECODE opening, carried into the block format. It is extended to the dense genesis pages and stacked per group.
What. The recursion guest cannot evaluate DECODE's five 2^20 preprocessed columns, nor the dense genesis pages (millions of rows), on its own. So each group's prepared tables (DECODE and the dense genesis pages chosen by
genesis_stack_plan) have their leading preprocessed columns stacked into one commitment.verify_block_whir, andverify_block_tree's plan. The prover's own roots only shortcut the prover's side.z.Negatives, on a guest with two dense genesis pages. Each is refused by the host verifier and by the recursion leaf, and admitted when the openings are skipped (the mutation):
Wrongly committed stacks are refused at the roots block: two pages swapped, a page holding another page's columns, another program's DECODE.
Cost. One stack per group costs +0.14 s of base (FAST 419; one commitment per table cost +0.49 s) and saves 0.57 s of recursion, by taking 90 k permutations out of the leaves.
BlockFormat::prepared = falseturns the openings off, for measurement only.3. ECDAS split; table heights capped
What.
split_ecdas).(round, op).Why. At a median block, one ECDAS table (2^19) argues on a 12 GiB tree. At p90 (2^20) it stacks into five polynomials on a 24 GiB tree.
Gates. FAST 534 and 535: the negatives, 3 mutations caught.
4. Recursion leaf: the leaf cap (G3) and the inverse share (W1)
LEAF_PERMS_CAP. With no fixed leaf count, it adds leaves while the heaviest leaf is over the cap. The block's own partition is unchanged.p · ediv(1, q), which has no satisfying assignment for q = 0 whatever p is. The formerediv(p, q)left the share free at p = q = 0 (≈ 2^-160 under GKR soundness).LFM_WHIR_SHARE_INVERSE=0keeps the former form.5. Batched argue, on by default since d9d0ac5 (
BlockFormat::argue = ArgueFormat::BATCHED; Mauro, 10-02: "batch the constraints")What. Each group's tables are argued together on the group's fork:
Verifier side. The verifier derives the bins from the statement's shapes and its own cap; the variant is never read from the proof. The proof carries one
BatchedArgueper group inBlockWhirProof.argues, andproof.tablesis empty under this format. The recursion leaves verify the same format (lane i-batch2, N-4).Security at the block's measured inputs (D-BATCH §3.2's formulas; re-checked at FAST 424's inputs: |T| ≤ 60 tables a group, ≤ 51 trees a bin, ≤ 2^28.87 input cells, bus messages ≤ 204 elements, N_C ≤ 413, D_max 4, n ≤ 21; L = 300):
Every term is above the WHIR phase, so the proof minimum is unchanged: 128.946 under the campaign accounting (130.393 for the WHIR fold under the calculator of record).
Measured.
The knob.
ArgueFormat::PerTable(one argument per table, the format before) stays measurable, withBLOCK_WHIR_ARGUE=per-tablein the real-block tests. At the per-table format, the MultiProof, the prepared openings and the partition are digest-equal to the head before the batched merge (BIG 393).6. KECCAK and ECSM split; their heights capped (the port of #1013's S0a; landed at 3cfffe2; approved by the lead under Mauro's any-block target, Mauro to confirm)
What.
split_keccak,split_ecsm), as ECDAS is at 2^17.Why. A keccak-heavy block at the gas limit makes about 2^21 permutation calls. One KECCAK table that tall stacks into eight polynomials of 2^27, against a group budget of three. At its cap each table fits one polynomial.
Bytes. Every block measured so far has KECCAK ≤ 2^17 rows and ECSM ≤ 2^11, so it builds the same tables and the same proof (FAST 830: digest 07d1bd43… unchanged on block 25368371).
Gates. FAST 830: KECCAK and ECSM forced into 4 tables each on block 25368371 prove and verify, base and tree; the count and height negatives; mutation C caught.
7. WHIR grinding 20 → 18 bits, queries 112 → 114 (landed at cbfa7d7; approved by Mauro, 10-05)
What.
Each WHIR chain grinds 18 bits instead of 20 before each round's queries, and opens 114 queries instead of 112 to buy the two bits back. At every block height (15 to 27 variables) Q =
num_queries(2, rounds, 128, 18).One site,
multilinear_prove::chain_config_under. Every side of the block reaches it throughBlockFormat::chain_config:verify_block_whir;The statement absorbs Q and the grind bits.
Scope: the block's WHIR proofs only. The recursion tree's own leaf, node and top proofs are STARK proofs (FRI) and keep their own grind.
It ports WHIR recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 32.62 s #1010's grind 18 (landed there at 2687e48). Opt-out:
LAMBDA_VM_ZF_WHIR_GRIND_BITS=20, which reproduces the previous proofs byte for byte.Security. The calculator of record: Johnson bound, η = 1/300, the fold proof of work unground.
Measured behind the knob, on c55dec4, one binary per box:
Bytes. The proof bytes change. Under the fixed trace hash and deterministic grind, the 1× top proof's digest is b9b4826d… at the default and 0da6fea9… under
=20. Both trees are accepted (ULTRA 015, at this head).Known limit. The leaf cap (279,000 permutations) sits above 2^18 LFM_HASH rows, and 18 bits moves every leaf about 1.7 % closer to that doubling.
Gates.
zf_format::; the chain refusals and the legacy-bytes KAT; the pins the flip moved; the host block refusal.One-binary A/B: the block tree vs #1010's epoch tree (FAST 416, noepoch/whir @ 454dad6)
Eight arms E B B E E B B E on the same binary (md5 checked after every arm):
Base, block 25368371 on FAST (each run against #1010's epoch base on the same binary)
Recursion (W3): proved and verified on block 25368371 (FAST 413)
lfm::whir_block::WhirBlockPlan) runs the host verifier's own statement checks, derives every shape from the AIR and every prepared root from the program, and never reads a proof. It prices each group in permutations and partitions the groups over the leaves (heaviest first, onto the least-loaded leaf).block_node, shared byte for byte with STARK no-epoch (prove-and-retire) prover: block 25368371 — work in progress #1013). They check the id, the state and the output equal across children, add the shares, and the top asserts zero.verify_block_tree(elf, statement, top)derives the top program and checks the top proof against it. Every preset is pinned inside: the base's options, the block format, the tree's options, the leaf rule and the fan-in.Every proof was verified by the harness off the clock. The base is unchanged by the emission running beside phase B (20.98 s vs 21.18 s in the arms without the change).
Next:
Base levers after the A/B (FAST 417–422, each S/P on one binary)
Memory (D-MEMORY, with i-mem / i-mem2)
drop_streamed_ops)layout_ahead, D-EXEC)Narrow trace storage (M4, lane i-m4)
Prover-only; the proof bytes are the same. The proof digest equals the head's before M4 (07d1bd43…) under the fixed trace hash + deterministic grind (FAST 820).
BlockOptions::narrow, productionNarrowing::CARD).Max RSS, wide → narrow (BIG 560; the traces themselves shrink about 4×, e.g. 24.89 → 6.20 GiB at 1×):
Before M4, #1014 ran out of memory at 3.03× (i-m4); the narrow line puts the 120.7 GiB edge near 5.5–6×.
Phase A uploads the next group beside the commit (3′, lane i-noepoch-w2)
Prover-only; the proof bytes are the same (digest 07d1bd43… at the default, FAST 832; the commits, their order and their bytes are unchanged).
BlockOptions::upload_ahead, on by default;BLOCK_WHIR_UPLOAD_AHEAD=0is the control).Streamed chunks laid out on three threads (E3 on by default, lane i-noepoch-w2)
Prover-only; the proof bytes are the same (digest 07d1bd43… at the default, FAST 838 and 835; the groups, their order and the packing are unchanged).
layout_workers0 → 3 inBlockOptions::production(59e9890). The streamed chunks are laid out on three threads, with at most K + 1 = 3 of them unpacked at a time (layout_ahead, E3), instead of on the builder's one layout thread.BLOCK_WHIR_LAYOUT_WORKERS=0(the inline layout, 01da99f's) is the control.Phase B's kept-top paths re-hashed in parallel (lever 1, lane i-noepoch-w2)
Prover-only; the proof bytes are the same (digest 07d1bd43… at the default, FAST 840 at 733557a — 82f9046 adds only the knob; the paths, their order and the refusal are unchanged).
BLOCK_WHIR_REHASH_SERIAL=1restores the serial re-hash (a measurement knob).BLOCK OPEN SPLIT(withLAMBDA_VM_BASE_SPLIT=1), phase B's openings by host stage and the kept-top gather and re-hash seconds.The tree's leaves execute while their artifacts are built (R2-i, lane i-noepoch-w2)
Prover-only; the proofs are the same (the top proof's digest equal with and without it, 0da6fea9…, under the fixed trace hash + deterministic grind, FAST 841).
prove_tree_pipelined, the way a prover would run it; there is no production tree driver yet). Its level 0 built all three leaves' artifacts first (three serial card holds, 0.24 s at 1×) and only then let the leaves execute and fill their traces (0.46 s until the first was ready) while the card sat idle (nsys timeline, FAST 839). Execution and fill do not read the artifacts; only the prove does.lfm_proveis now cut into its host half (lfm_execute_and_fill) and its card half (LfmFilled::prove, which asserts the artifacts' hasher is the one the traces were filled for), in the same order; the harness builds the artifacts on a thread of their own and each leaf executes and fills beside them, waiting for its artifacts only to prove.W3_EXEC_BESIDE_ARTIFACTS=0is the control (the order before).A second whole-block field. The W3 readout prints, on the clock between the base and the tree, the block report, a second block frame for the LT heights and the group tables: 0.13–0.14 s at 1× that a prover would not spend. "Whole block" keeps its meaning (every number above includes them); from d169edd on,
W3 RECURSIONalso prints "whole excl. harness readouts" beside it (at d169edd, FAST 841 + 842 pooled: whole 18.54 s, whole excl. harness readouts 18.40 s).The rest laid out in waves; KECCAK_RND built as its tables (W, lane i-m4b)
Prover-only; the proof bytes are the same (digest 07d1bd43… under the fixed trace hash + deterministic grind: FAST 854 at 0bcc1fc, and FAST 855's W arm on this head's code).
BlockOptions::rest_layout_bytes). The tables, their order and the groups are the same (test).split_keccak_rndthen copied into its 2^16-row tables. At 4.13× that copy was a second peak of the same height. The finish now builds the 2^16-row tables directly (BlockOptions::finish_keccak_rnd_chunks), the same tables as the split's (test), and hands none out during the windows, which would change the groups.BLOCK_WHIR_REST_LAYOUT=allandBLOCK_WHIR_KR_FINISH_CHUNKS=0restore the old behaviour.pack_rest_as_laid_out) was re-measured with the waves: no gain (+0.01 s), so it stays off.LAMBDA_VM_BLOCK_MEMLOG=1(off by default). It prints the host memory term by term every half second and at each phase mark, with the line at jemalloc's active peak and each arena's bytes (those two in the lib tests, which install jemalloc).BLOCK REST TABLES(each rest table's layout end and group) and each group's commit start (from@).The tree's first finished leaf executes during phase B (R2-ii, lane i-noepoch-w2)
Prover-only; the proofs are the same (base digest 07d1bd43… and the top proof's digest equal with and without it, 0da6fea9… — FAST 841's — under the fixed trace hash + deterministic grind: FAST 845, and FAST 847 again on fac261f, the merge with W).
block_prove_on_forks_observed; the old entry point passes a no-op, and the proof is the same with any observer). A leaf's arena is built from its groups' words alone (group_arena_words+leaf_arena;block_leaf_arenais built from them). The W3 harness turns the groups into words as they arrive; the first leaf whose groups are all opened while another group is still to come (leaf 0 = groups 1, 5, 6 at 1×, done after group 6) executes and fills its traces on a thread of its own, about 1.5 s before the base ends, and the tree picks it up. Off the clock its arena is checked against the finished proof's.W3_LEAF_DURING_PHASE_B=0is the control.The finish's tables packed as they are built (b2, lane i-m4b)
Prover-only; the proof bytes are the same (digest 07d1bd43… under the fixed trace hash + deterministic grind at both arms: FAST 855 at 0cebe16, and FAST 857 again on 365e3ab, the merge with R2-ii).
BlockOptions::pack_finished). KECCAK_RND is packed in waves of four 2^16-row tables. Phase A takes those tables as narrow columns and uploads them as they are, so the card packs only the groups' other tables. Nothing packed is transposed.BLOCK REST PACKEDcounts the rest: 187 of 191 tables at 4.13×).BLOCK_WHIR_PACK_FINISHED=0restores W.Measurement posture: the card's pool now retains freed memory (baseline shift)
Not a prover change; the proofs are the same (the top proof's digest 0da6fea9… under both postures, fixed trace hash + deterministic grind, FAST 848; 351a773 adds only a test readout).
LAMBDA_VM_MEMPOOL_RELEASE_MB=0. The card's stream-ordered memory pool then hands its freed blocks back to the driver at each synchronize, so a VRAM sampler's total − free reads the live working set. The code default is to retain every freed block (DEFAULT_MEMPOOL_RELEASE_THRESHOLD_BYTES = u64::MAXin math-cuda), and that is what a prover runs.cuStreamSynchronizeandcuMemAllocAsyncwhile the card was idle was ≈ 0.25 s in phase A, 0.42 s in phase B (0.26 s of it in the encode: one 18–33 ms gap per group) and 0.34 s in the tree.W3 DEVICEline).The prover refuses a partition over the group maximum (lane i-m4b)
Prover-only; the proof bytes are the same (digest 07d1bd43…, FAST 858). The prover now refuses a block over
BlockFormat::max_groupsas its groups close, with the verifier's ownInvalidTableCountserror, instead of proving a block the verifier refuses. The median block (90 groups against the cap of 64) spent its whole ≈ 190 s base on such a proof (BIG 564). A test covers both prover paths, with a mutation for each check.The tree's nodes built beside it, each level proving as its nodes arrive (A, lane i-noepoch-w2)
Prover-only (the W3 harness); the proofs are the same (the top proof's digest 0da6fea9… — FAST 841's — with and without it, under the fixed trace hash + deterministic grind: FAST 889, and FAST 891 again after the permit fix below).
prove_tree_pipelined) built every node program and its artifacts on one thread, level after level, and level 0 joined that thread before any node proved, so level 1 waited for the whole tree's builds. At the median block, 32 s of serial node builds after the leaves' artifacts held level 0 open 10.7 s past its last leaf proof, and the card sat idle 11.4 s before level 1 (BIG 565 / 568's card trace). At 2.66× the wait was 1.5–2.1 s (FAST 888).W3_EMIT_THREADSthreads (default 4, the builder's own: on the global pool a prover's join can steal an emission and leave the card idle, STARK no-epoch (prove-and-retire) prover: block 25368371 — work in progress #1013's FAST 454), and the builder's thread builds each one's artifacts as it arrives. Each node proves once its children are proved and its slot is filled. A builder that stops fails every empty slot.W3_NODE_PIPE=0is the control.Published<T>serves as the slot; there is no per-group early emission (W3 builds every leaf's artifacts up front, so a level's programs are emitted together); and there is no host-only thread marking (WHIR no-epoch (prove-and-retire) prover: block 25368371 — work in progress #1014 has none).build_levels, an emit on the pool and a finish on the builder's thread). A toy tree at the median's shape puts the serial builder's programs in their slots whatever order a pool finishes them in, and finishes every node off the rayon workers (test; finishing on a worker, or publishing in arrival order, fails it). A failed build fails every slot above it without a hang (test).WhirBlockPlan::programsbuilds as rayon jobs.W3_NODE_TIMES=1(off by default). It prints, per program, when it was built, taken and proved; its prove's split (execute, fill, the prove net of the card wait, the wait); and each node level's start against the level below. The stamps are taken either way and cost a handful ofInstantreads.prove_tree_pipelinedis its de-facto driver. With the slots it now has a driver's shape: leaves from phase B, nodes from slots, levels as their nodes and children arrive. Moving it out of the test harness is a landing item for STARK no-epoch (prove-and-retire) prover: block 25368371 — work in progress #1013 and WHIR no-epoch (prove-and-retire) prover: block 25368371 — work in progress #1014 both.Each node proved as soon as its own children are (C, lane i-noepoch-w2)
Prover-only (the W3 harness); the proofs are the same (the 1× top proof's digest with and without it, under the fixed trace hash + deterministic grind, both trees accepted: 0da6fea9…, BIG 614 — the digest FAST 841 / 889 / 891 printed).
siblingsworkers proves every program of the tree, leaves and nodes, taking them in topological order (the leaves, then each node level) and publishing each proof into a slot of its own. A node waits only for its own children's slots, so it executes, fills and proves while the rest of the level below still proves.W3_DATAFLOW=0is the control: each node waits for its whole level below (tested never to start early).W3 LEVELwall now runs from the level below's last proof to its own.The held tables spill to disk, by default only when memory is short (lane i-m4b)
Prover-only; the proof bytes are the same: one shape and one proof digest (07d1bd43…) across the base and all four policies, under the fixed trace hash + deterministic grind (BIG 616). The 1× top proof's digest (0da6fea9…) and the tree verify at the landed merge (ULTRA 006).
crypto/stark/src/spill.rs) is imported byte-identical; it digests each slot and writes it with O_DIRECT on a writer thread, off the committer's path. A table moves only when the writer's queue has room at that moment, so the committer never waits.SpillFailed). After a group's opening its packed columns are let go.LAMBDA_VM_BLOCK_SPILL=auto(the default) |off|always|<GiB>(a resident budget).autospills a table when the host's bytes plus a reserve plus the table would pass the target.LAMBDA_VM_BLOCK_SPILL_TARGET_GIB, else min(the cgroup's limit, v2 or v1;MemTotal) − 10 GiB.BLOCK SPILLprints the policy, the slots and bytes, the writer's split, the read-back, and the largest host readingautodecided on.always(BIG 566, single runs): 22.74 GiB spilled, max RSS 52.53 → 40.12 GiB, whole block +1.15 s, drivers waited 0 s.auto(BIG 567): by default nothing spills (target 110.7 GiB). Under a 35 GiB target it spills 21.21 GiB, max RSS 41.04 GiB, +2.91 s.autospilled 26.98 GiB from group 44 of 90, and the tree verified.auto, O =off, S =always, T =autoat a 47.5 GiB target):autorun spilled 0 in both jobs, at 110.7 GiB and under the 47.5 GiB target (FAST's limit, kept as a real test on BIG's 128 GiB; the host read 25.3–26.8 GiB across those runs);alwaysandautoat 0 spilled within noise.autospilled 0 (host at most 27.65 GiB).Phase 4 counts the BITWISE lookups in slices (#1013's c369843, lane i-m4b)
Prover-only; the bytes are the same:
What changes:
LAMBDA_VM_P4_SLICED=0keeps the whole-source collectors. The knob is WHIR no-epoch (prove-and-retire) prover: block 25368371 — work in progress #1014's only, for the A/B.Measured: the median, BIG 619. One binary on the cap-128 exploration head, N P P N,
autospill on. N runs the whole-source path, P the slices.auto)autospills only once memory is short.The top executes each child's share as that child is proved, while a child is still unproved (B and B′, lane i-noepoch-w2)
Prover-only (the W3 harness and the LFM executor); the proofs are the same. The 1× top digest is 0da6fea9… with the streamed top on and off, under the fixed trace hash + deterministic grind, and both trees are accepted (BIG 617; ULTRA 008 and 009; ULTRA 011 at c55dec4 itself).
executor::StreamedExecutionruns an execution as its arena groups land: each instruction runs in the wave in which the last group it reads lands (each instruction's group set comes from one forward pass), in the level schedule's order, into the slot the schedule gives it. So the witness isexecute's, word for word.finishchecks that every instruction ran once. Dropping the group propagation (ReadBeforeWrite) or re-running instructions across waves (DoubleWrite) fails them.W3_STREAM_TOP, on by default), so only the last child's share and the fill remain after the last child.W3 TOP EXECUTEprints which. A test covers a program ready before the last child (streamed), after it (whole), and a failed child (whole, which then reports the failure). Inverting the predicate fails the test.A node executes from its program; only its prove waits for its artifacts (b′, lane i-noepoch-w2)
Prover-only (the W3 harness); the proofs are the same: the 1× top digest is 0da6fea9… with
W3_EXEC_EARLYon and off, under the fixed trace hash + deterministic grind, and both trees are accepted (ULTRA 012; ULTRA 013 at 806c211 itself).node_flow). The traces are filled under the block hasher, which the node artifacts are built for. The top's streaming choice (B′) is taken when the top can execute.W3_EXEC_EARLY=0is the control.LfmProveError::HasherMismatch, naming both) instead of failing a release assert, and the streamed execution's finish returns an error instead of asserting its public words' capacity. Each has a test and a mutation.